S, w ⊨ A

$ S, w\models A

クリプキ構造$ S、世界$ w\in Wの元で、論理式$ Aが成り立つ

$ Aが$ \Boxを含まなければ、通常の命題論理と同じ

各世界の真偽は独立に成り立つ

$ Aが必然性演算子▢を含むと、世界間の真偽が絡み合うことになる

$ \Box Aが、$ wで真になるためには、

$ wから到達できる任意の世界$ w'で、$ Aが真になるということ

つまり、以下2つは同値

$ S,w\models\Box A

$ wRw'を満たす任意の$ w'\in Wに対して$ S,w'\models A

$ w\models Aのように書いた場合、以下のように場合分けができる

①$ wから到達可能な世界$ w'が0個である

②$ wから到達可能な世界$ w'が1個以上ある

②-1 全ての世界$ w'で$ w\models Aが成り立つ

②-2 全てではないが1つ以上の世界$ w'で$ w\models Aが成り立つ

②-3 どの世界$ w'でも$ w\models Aは成り立たない

↑のように場合分けした時、

$ w\models \square Aが成り立つのは、①と②-1

$ w\models \Diamond Aが成り立つのは、②-1と②-2

①は成り立たない、なぜなら

到達可能な世界が0個のとき、

$ w\models \square Aが成り立つ

この時、$ w\models \square \lnot Aも成り立つ

従って、$ w\models \lnot\square\lnot Aは成り立たない

$ \Diamond A:= \lnot\Box\lnot Aなので、①は成り立たない

ということは、∃x. Pxは、∀x. Pxを含意するのイメージは成り立たないのかmrsekut.icon

そもそもイメージで、$ \forall,\existと$ \square,\Diamondは全く別物なので、そらそうだろと言われればそうなのだが